A method has been known that performs a determination process of a logical formula that includes a logical disjunction or a logical conjunction of one or plural statements by using a binary decision diagram (BDD). In the method, when the logical formula is received, a BDD is formed based on the received logical formula. A BDD defines a determination order of statements included in a logical formula and also defines determination results (“true” or “false”) of a statement that is a next determination target or the entire logical formula for both determination results of “true” and “false” of each statement.
For example, a method has been known that increases the possibility that a cost of a determination process of an entire logical formula decreases by using a BDD in which a statement with a lower calculation cost of the determination process is first determined. For example, Japanese Laid-open Patent Publication No. 2009-211312 is known as related art.